타입 유니버스

타입 유니버스(type universe)는 타입들의 타입이다.

정의 방식

러셀 스타일 유니버스

러셀 스타일에서는 유니버스 $\mathcal{U}$에 속하는 대상이 곧 타입이다. $$\mathcal{U}\text{type}\begin{array}{c}\begin{array}{c}A:\mathcal{U}\end{array}\\ A\text{type}\end{array}$$

타르스키 스타일 유니버스

타르스키 스타일에서 유니버스 $\mathcal{U}$에 속하는 대상들은 타입의 부호(code)이며, 이 부호에 대응하는 타입을 주는 함수 $\mathcal{T}$가 함께 주어진다. $$\mathcal{U}\text{type}\begin{array}{c}\begin{array}{c}\check{A}:\mathcal{U}\end{array}\\ \mathcal{T}(\check{A})\text{type}\end{array}$$

유니버스 계층

아래 내용은 러셀 스타일을 따라 서술하였다. 유니버스 타입 $\mathcal{U}$가 들어가는 유니버스가 필요하다면, $\mathcal{U}$보다 큰 새로운 유니버스 ${\mathcal{U}}^{\prime }$이 필요하다. 그러나 ${\mathcal{U}}^{\prime }$이 들어가는 유니버스가 필요한 경우, 이보다 더 큰 또 다른 유니버스 ${\mathcal{U}}^{″}$을 도입해야 한다. 이와 같은 과정을 무한히 반복하면 다음과 같은 유니버스 계층(universe hierarchy)이 얻어진다. $$\begin{array}{c}{\mathcal{U}}_0:{\mathcal{U}}_1\\ {\mathcal{U}}_1:{\mathcal{U}}_2\\ {\mathcal{U}}_2:{\mathcal{U}}_3\\ ⋮\end{array}$$

누적성

러셀 스타일 유니버스 계층을 갖춘 타입이론에서 누적성(cumulativity)은 다음을 가리킨다. $$\begin{array}{c}\begin{array}{c}A:{\mathcal{U}}_i\end{array}\\ A:{\mathcal{U}}_{i+1}\end{array}$$ 누적성은 타입이론을 사용하기 편리하게 만들어주지만, 타입의 유일성이 성립하지 않게 만든다.